We have a category for Theory/Lambda Calculus, but none for Theory/Pi and related calculi. Not sure, what the specific name should be, though.

There are plenty of academic papers about Haskell, and plenty of informative pages on the Haskell Wiki. But there's not much between the two extremes. The Monad.Reader aims to fit in there; more formal than a Wiki page, but less formal than a journal article.

Want to write about a tool or application that deserves more attention? Have a cunning hack that makes coding more fun? Got that visionary idea people should know about? Write an article for The Monad.Reader!

Contact Shae Erisson ( shae@ScannedInAvian.com ) to become an author, or talk to shapr on the #haskell irc channel on irc.freenode.net.

Check the current roster - http://www.haskell.org/hawiki/TheMonadReader

Publishing Format:

• Input is LaTeX (or just plaintext and images).
• Output is Web and PDF/PS.
• Release once a month.
• Each article in a darcs repo for easy collaboration between author and editor.

License:

• BSD-like, feel free to read it, teach it, hack it, copy it, improve it.

The Monad.Reader: sequencing your input since 2005

I've begun to get interested in a language-based approach to network protocol development. There are some nice ones like Prolac and older ones like Estelle.

I'm systematically boiling down an RFC to an implementation, assuming such a thing is possible, and am looking for all approaches. I'm less interested in formal verification techniques that don't result in a usable piece of software, but all pointers are appreciated. I'd like to hear your experience with such techniques too. I'm looking at whatever google and citeseer spit out for "protocol languages" and "protocol compilers".

What is the relation between programming languages, model theory, and proof theory? I heard proof theory is more concerned with "syntax" whereas model theory is more concerned with "semantics". Would it be true to say that operational semantics corresponds to proof theory and denotational semantics to model theory? If yes, how exactly do they relate to each other?

By the way, a small related question: What exactly is a "theory" when someone says, he developed (say) a "Theory of Objects" like Abadi/Cardelli?

GCC wiki

Why do I feel like a kid in a candy store?

The following is from my latest project which is a foray into functional programming. Any comments or suggestions?

The Unimperative Programming Language

by Christopher Diggins

Introduction

Unimperative is a simple programming language, which supports a mix of procedural programming and functional programming. In Unimperative the primary data type is a function. The sequence of evaluation in Unimperative matters somewhat, and function parameters are evaluated left to right.

Unimperative has a surprise twist, which I will save for the end

Comparing to Scheme

Unimperative is quite similar to Scheme. In Scheme we can write a factorial function as:

  (define factorial
    (lambda (n)
      (if (zero? n)
          1
          (* n (fact (- n 1))))))

In Unimperative we can write the equivalent function as:

  Function factorial =
    (IfZero, _1,
      1,
      (Mult, _1, (Self, (Dec, _1))));

Basic Usage

In many language we call functions by writing:

  MyFxn(x, y)

In the Unimperative programming language we instead write:

  (MyFxn, x, y)

The first element following an open paranthesis, and followed by a comma, is always treated as a function which will be evaluated. The elements which follow are passed as arguments to the function.

Other functions after the first one in a list are not evaluate:

  (MyFxn, OtherFxn)

This evaluates the function MyFxn and passes the OtherFxn as a parameter without evaluating it.

A function must be followed by at least one argument in order to be evaluated. The evaluation operator is the combination of paranthesis and comma:

  (xxx,

The following code does not evaluate MyFxn:

  (MyFxn)

If we wanted to evaluate MyFxn we would have to write:

  (MyFxn, nil)

Alternatively we could also write:

  (Eval, MyFxn)

Defining Functions

To define a function in Unimperative we do so as follows:

  Function MyFxn = (Add, _1, _2);

The _1 and _2 are place holders which refer to the first and second argument respectively.

An Interesting Twist

The Unimperative programming language has a surpise: it is completely legal C++, and doesn't use any macros! An Unimperative library will be available soon as part of the next OOTL ( Object Oriented Template Library ) release from http://www.ootl.org

There ought to be a word for the sinking realization that, semantically, the language you've been designing and implementing for months is only a small extension over the one you're implementing it in.

(I posted about this language once before. Writing an interpreter for it in Scheme was one thing; but, once I started to compile it down to Scheme, and saw how easy it was--the generated Scheme code was a pretty trivial transform from the ASTs--I realized that meant my semantics offered very little over Scheme's. I'll probably stick with it as an exercise, but that's about all the value it offers at this point.)

Garbage collection has improved greatly over the years, but there are worst cases which are still difficult to avoid without writing your own custom memory management system. For example, let's say you have 128MB of 3D geometry data loaded in Haskell/OCaml/ML-NJ/Erlang/Lisp/YourFavoriteLanguage. This data is in stored in the native format of your language, using lists and tuples and so on. At some point, the GC is going to go through that 128MB of data. Generational collection delays this, but it some point it will still happen. Or do any systems handle this situation gracefully?

The best I've seen in this regard is Erlang, because each process has its own heap, and those heaps are collected individually. But if you put 128MB of data in one heap, there will still be a significant pause. Perhaps Erlang's GC is still better than most in this regard, as there a single-assignment language creates a unidirectional heap which has some nice properties.

And then of course there are the languages with reference counting implementations, which perform better than languages with true GC in this regard.

Thoughts?

Any good suggestions for something like that? i.e, Hibernate but for C++.

I am looking for a product/solution that can be used in production work, so it must be stable, supported etc.

Perhaps this can be made part of a FAQ.

There are many abbreviations used on LTU which are neither obvious, nor part of the computer science lexicon. To aid new readers, I propose a glossary of such.

To start off the list:

CTM: Concepts, Techniques and Models of Computer Programming by PVR
PVR: Peter van Roy
LTU: Lambda the Ultimate (in case there was any doubt)
SICP: Structure and Interpretation of Computer Programs by Abelson and Sussman

Lots more, I'm sure... please add to the list.